FDL - Step of Proof: hd-before

Step of Proof: hd-before

Inference at *
Iof proof for Lemma hd-before:

T:Type, L:(T List). (0 < ||L||)

(

x:T. (x

L)

(

(x = hd(L)))

hd(L) before x

L)

by ((Auto)

CollapseTHEN (((DVar `L')

CollapseTHEN (((All Reduce)

CollapseTHEN (Auto'))

))

))

C

C1:

C1: 1. T : Type

C1: 2. u : T

C1: 3. v : T List

C1: 4. 0 < (||v||+1)

C1: 5. x : T

C1: 6. (x

[u / v])

C1: 7.

(x = u)

C1:

u before x

[u / v]

C.

Definitions P Q, s = t, hd(l), A, (x l), a < b, type List, Type, ||as||, i j , x:A. B(x), x:AB(x), x before y l

Lemmas l member wf, not wf, l before wf